g:IAbMonoid, n:. IsMonHom{g,g}(a.n  a) 

latex

Up	groups 1
Definitions of Statement	IMonoid, IAbMonoid, IsMonHom{M1,M2}(f)
Definitions	t  T, FunThru2op(A;B;opa;opb;f), P & Q, IsMonHom{M1,M2}(f), x:A. B(x), IMonoid, IAbMonoid
Lemmas	iabmonoid wf, nat wf, mon nat op id, grp car wf, mon nat op op